package trabajoISW2.domain.contracts;

import java.util.List;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Query;
import trabajoISW2.domain.implementations.Book;

@Inv("getSubjectId() >= 0")
public interface ISubject {

	@Pre("subjectId >= 0 && subject <= Integer.MAX_VALUE #WrongIdException")
	@Pos("getSubjectId() == subjectId")
	public void setSubjectId (int subjectId);
	
	@Query
	public int getSubjectId ();
	
	@Pre("name.compareTo(\"\") != 0 && name != null #WrongNameException")
	@Pos("getName() == name")
	public void setName (String name);
	
	@Query
	public String getName();
	
	@Pre("books != null #IllegalArgumentException")
	@Pos({"getBooks().compare(books) == 0"})
	public void setBooks (List<Book> books);
	
	@Query
	public List<Book> getBooks();
	
	@Pre({"book !=null #IllegalArgumentException"})
	@Pos({"!getBooks().contains(book)@Pre==>getBooks().size() == getBooks().size()@Pre + 1 && getBooks().contains(book)",
		  "getBooks().contains(book)@Pre ==> getBooks().size() == getBooks().size()@Pre"})
	public void addBook (Book book);
	
	@Pre("book != null")
	@Pos({"!getBooks().contains(book)@Pre ==> getBooks().size() == getBooks().size()@Pre",
		   "getBooks().contains(book)@Pre ==> getBooks().size() == getBooks().size()@Pre -1 && getBooks().contains(book)"})
	public void removeBook (Book book);

}
